package naruto.datastructures.graph;

import java.io.File;
import java.io.IOException;
import java.io.PrintWriter;
import java.util.Hashtable;
import java.util.Vector;
import naruto.datastructures.instruction.*;
import naruto.datastructures.trace.*;
import naruto.common.*;

/**
 *
 * @author nacuong
 */
public class IfCompleteModel extends Graph<IfCompleteNode> {

  /**
   * Merge an if complete trace into the model
   * @param icTrace
   */
  public void mergeTrace(IfCompleteTrace icTrace){
    if (icTrace.isEmpty())
      return;
    /* add new nodes into model */
    addNewNodes(icTrace);
    /* connect new edges in model */
    connectNewEdges(icTrace);
    /* add final nodes */
    addFinalNode((IfCompleteNode)this.getNode(icTrace.lastElement()));
    /* set initial node */
    if (!this.hasInitialNode())
      this.setInitialNode((IfCompleteNode)this.getNode(icTrace.firstElement()));
  }

  /**
   * Add new node from an if complete trace into the model
   * @param icTrace
   */
  private void addNewNodes(IfCompleteTrace icTrace){
    for (IfCompleteInstruction icInstruction: icTrace){
      IfCompleteNode icNode;
      if (icInstruction instanceof IfInstruction)
        icNode = new IfNode((IfInstruction) icInstruction);
      else if (icInstruction instanceof MethodInstruction)
        icNode = new MethodNode((MethodInstruction) icInstruction);
      else
        icNode = new EndIfNode((EndIfInstruction)icInstruction);

      if (!this.contains(icNode))
        this.add(icNode);
    }
  }

  /**
   * Connect new edges that appear in the if complete trace into the model
   * @param icTrace
   */
  private void connectNewEdges(IfCompleteTrace icTrace){
    IfCompleteNode current = (IfCompleteNode)this.getNode(icTrace.firstElement());
    if (this.getInitialNode() == null)
      this.setInitialNode(current);

    for (int inx = 1; inx < icTrace.size(); inx++){
      IfCompleteInstruction icInsn = icTrace.get(inx);
      IfCompleteNode next = (IfCompleteNode)this.getNode(icInsn);
      if (next instanceof IfNode)
        next.setInstruction(icInsn);

      this.connect(current, next);    
      current = next;
    }
  }

  /**
   * Refine the model so that it looks more like a CFG and
   * it contains abstract edges.
   */
  public void refine(){
    for (IfCompleteNode icNode: this){
      if (icNode instanceof EndIfNode){
        deleteLoopEndFor((EndIfNode)icNode);
        createFalseForEdge((EndIfNode)icNode);
        connectEndForAndFor((EndIfNode)icNode);
      }
      fixPreEndforEdge(icNode);
      if (icNode instanceof IfNode)
        createAbstractEdge((IfNode)icNode);
    }
  }

  /**
   * This refinement connects all endfor with its corresponding for node.
   * @param endIfNode
   */
  private void connectEndForAndFor(EndIfNode endIfNode){
    if (endIfNode.isEndForLoopNode(this)){
      IfNode forNode = endIfNode.getIfNode(this);
      Edge edge = new Edge(endIfNode, forNode, GraphCommon.EdgeStatus.CONCRETE);
      if (!endIfNode.contains(edge))
        endIfNode.addEdge(edge);
    }
  }

  /**
   * This refinement deletes all edges of the form endif_i -> endif_i
   * @param endIfNode the source endif node
   */
  private void deleteLoopEndFor(EndIfNode endIfNode){
    if (endIfNode.isEndForLoopNode(this)){
      int inx = 0;
      Vector<Edge> edges = endIfNode.getOutcomingEdges();
      while (inx < edges.size()){
        Edge edge = edges.get(inx);
        if (edge.getTarget().equals(endIfNode))
          edges.remove(inx);
        else
          inx++;
      }
    }
  }

  /**
   * This refinement transforms all the pair (node -> for_i) and
   * (node -> endfor_i) to (endfor_i -> for_i) and (node -> endfor_i)
   * @param node the node to be considered
   */
  private void fixPreEndforEdge(Node node){
    Vector<Edge> edges = node.getOutcomingEdges();
    int inx = 0;
    while (inx < edges.size()){
      Edge edge = edges.get(inx);
      Node target = edge.getTarget();
      if (target instanceof IfNode && ((IfNode)target).isLoopNode()){
        EndIfNode endForNode = ((IfNode)target).getEndIfNode(this);
        if (node.connectTo(endForNode)){
          edges.remove(inx);
          continue;
        }
      }
      inx++;
    }
  }

  /**
   * This refinement create false edge from for loop. That means
   * it transform all edges of the form (endfor_i -> a) into
   * (for_i -> a). It will preserve the edge from (endfor_i -> for_i).
   * 
   * @param endIfNode
   */
  private void createFalseForEdge(EndIfNode endIfNode){
    if (endIfNode.isEndForLoopNode(this)){
      IfNode ifNode = endIfNode.getIfNode(this);
      for (Edge edge: endIfNode.getOutcomingEdges()){
        Node target = edge.getTarget();
        if (!target.equals(ifNode)) {
          Edge falseForEdge = new Edge(ifNode, target, GraphCommon.EdgeAttribute.FALSE, GraphCommon.EdgeStatus.CONCRETE);
          if (!ifNode.contains(falseForEdge))
            ifNode.addEdge(falseForEdge);
        }
      }

      endIfNode.getOutcomingEdges().clear();
    }
  }

  /**
   * This refinement create an abstract edge between an ifnode and
   * its corresponding endif node, given the condition that this path
   * has not been traversed by the if complete model
   * @param ifNode
   */
  private void createAbstractEdge(IfNode ifNode){
    if (!ifNode.isLoopNode())
      if (!ifNode.traverseFalseBranch()){
        Edge edge = new Edge(ifNode, ifNode.getEndIfNode(this), GraphCommon.EdgeAttribute.FALSE, GraphCommon.EdgeStatus.ABSTRACT);
        ifNode.addEdge(edge);
      } else if (!ifNode.traverseTrueBranch()){
        Edge edge = new Edge(ifNode, ifNode.getEndIfNode(this), GraphCommon.EdgeAttribute.TRUE, GraphCommon.EdgeStatus.ABSTRACT);
        ifNode.addEdge(edge);
      }
  }

  /**
   * Translate the model and the specification into a smv file.
   * SMV file is input of NuSMV model checker.
   * @param filePath  the location of the output file
   * @param ltlSpecification  the specification to be checked by the model checker
   * @param methodToName  a mapping between method name and its mock variable to be represented in smv file
   */
  public void toSMV(String filePath, String ltlSpecification, Hashtable<String,String> methodToName){
    Vector<String> methodCallList = getMethodCallList();
    File file = new File(filePath);
    file.delete();
    /*append method mock name with predicate*/
    for (String methodName: methodToName.values())
      ltlSpecification = ltlSpecification.replaceAll(methodName, "predicate="+methodName);
    
    try {
      file.createNewFile();
      PrintWriter out = new PrintWriter(file.getAbsolutePath());
      out.print("MODULE main \n" +
              " VAR\n   predicate : {");
      for (String methodCall: methodCallList)
        out.print(methodToName.get(methodCall) + ", ");
      out.println("NONE};");
      
      out.print("   state : {");
      for (int inx = 0; inx < this.size(); inx++)
        out.print("node" + inx + ", ");
      out.println("node" + this.size() + "};");

      out.println(" ASSIGN");
      if (this.hasInitialNode()){
        out.println("   init(state) := node" + this.indexOf(initialNode) + ";");
        out.print("   init(predicate) := ");
        if (initialNode instanceof MethodNode)
          out.println(methodToName.get(((MethodNode)initialNode).getInstruction().getMethodName()) + ";");
        else
          out.println("NONE;");
      }

      out.println("   next(state) :=" );
      out.println("     case");
      for (Node node: this){
        out.print("       state = node" + this.indexOf(node) + " : {");
        Vector<Node> outcomingNodes = node.getOutcomingNodes();
        for (int inx = 0; inx < outcomingNodes.size(); inx++){
          out.print("node"+ this.indexOf(outcomingNodes.get(inx)));
          if (inx != outcomingNodes.size()-1) out.print(", ");
        }
        if (isFinalNode((IfCompleteNode)node))
          out.print(", node" + this.size());
        out.println("};");
      }
      out.println("       state = node" + this.size() + " : {node" + this.size() + "};");
      out.println("       esac;");

      out.println("     next(predicate) :=");
      out.println("       case");
      for (Node node: this){
        out.print("         state = node" + this.indexOf(node) + " : ");
        if (node instanceof MethodNode)
          out.println(methodToName.get(((MethodNode)node).getInstruction().getMethodName()) + ";");
        else
          out.println("NONE;");
      }
      out.println("         state = node" + this.size() + " : NONE;");
      out.println("     esac;");
      
      out.print("LTLSPEC (");
      out.print("(F state = node" + this.size() + ") & " + ltlSpecification + ")");
      out.close();
      
    } catch (IOException e){
      System.out.println(e);
    }
  }

  private Vector<String> getMethodCallList(){
    Vector<String> methodCallList = new Vector<String>();
    for (Node node: this)
      if (node instanceof MethodNode){
        String methodName = ((MethodNode)node).getInstruction().getMethodName();
        if (!methodCallList.contains(methodName))
          methodCallList.add(methodName);
      }

    return methodCallList;
  }

}
